es:event_system{i:l}, e:es-E(es), l:IdLnk, tg:Id.
(es-kind(es; e) = rcv(l,tg)  Knd)
 guard(((loc(e) = destination(l)  Id)  (loc(es-sender(es; e)) = source(l)  Id))) 

latex

Definitions	x:A. B(x), P  Q, t  T, prop{i:l}, rcv(l,tg), b, es-isrcv(es; e), isrcv(k), sq_type(T), guard(T), isl(x), tt, if b then t else f fi , True, P  Q, ||as||, Y, decidable(P), P  Q, es-lnk(es; e), lnk(k), t.1, outl(x)
Lemmas	Knd wf, es-kind wf, rcv wf, Id wf, IdLnk wf, es-E wf, event system wf, Knd sq, decidable equal Id, es-loc wf, ldst wf, es-sender wf, lsrc wf, es-axioms, es-index wf, length wf1, es-Msgl wf